<html>
<head><meta charset="utf-8"><title>Understanding atomic ordering · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html">Understanding atomic ordering</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="207561701"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207561701" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207561701">(Aug 20 2020 at 19:07)</a>:</h4>
<p><a href="https://doc.rust-lang.org/core/sync/atomic/fn.fence.html#examples">https://doc.rust-lang.org/core/sync/atomic/fn.fence.html#examples</a><br>
Shouldn't the spinlock use Release ordering to make sure that it notifies other threads of lock acquiring and Acquire to make sure it has the most recent flag?<br>
Synchronization is only guaranteed on release store + acquire read (at least that's what I understand from <a href="https://en.cppreference.com/w/cpp/atomic/memory_order">C11 memory ordering</a>)</p>



<a name="207565414"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207565414" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207565414">(Aug 20 2020 at 19:39)</a>:</h4>
<p>The example uses release/acquire fences, not loads and stores. I don't see anything on the cppreference page about release fences but it might be a factor</p>



<a name="207566911"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207566911" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207566911">(Aug 20 2020 at 19:53)</a>:</h4>
<p><a href="https://llvm.org/docs/Atomics.html#atomic-instructions">LLVM</a> says:</p>
<blockquote>
<p>A fence provides Acquire and/or Release ordering which is not part of another operation; it is normally used along with Monotonic memory operations. A Monotonic load followed by an Acquire fence is roughly equivalent to an Acquire load, and a Monotonic store following a Release fence is roughly equivalent to a Release store.</p>
</blockquote>
<p>Note that a "monotonic load" is rust's <code>load(Relaxed)</code> and "monotonic store" is <code>store(_, Relaxed)</code></p>



<a name="207567724"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207567724" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207567724">(Aug 20 2020 at 20:00)</a>:</h4>
<p>By the way, I think the documentation and diagram in <a href="https://doc.rust-lang.org/core/sync/atomic/fn.fence.html">https://doc.rust-lang.org/core/sync/atomic/fn.fence.html</a> is not very good.</p>
<blockquote>
<p>A fence 'A' which has (at least) <code>Release</code> ordering semantics, synchronizes with a fence 'B' with (at least) <code>Acquire</code> semantics, if and only if there exist operations X and Y, both operating on some atomic object 'M' such that A is sequenced before X, Y is synchronized before B and Y observes the change to M. This provides a happens-before dependence between A and B.</p>
</blockquote>
<p>None of the terms used in this paragraph are defined or linked except for doc links for <code>Ordering::Release</code> and <code>Ordering::Acquire</code>. It is followed by a diagram with two arrows and no explanation of what those arrows represent</p>



<a name="207567853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207567853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207567853">(Aug 20 2020 at 20:01)</a>:</h4>
<p>ideally we would link to a section in the rust book on memory ordering but I think there is no such thing</p>



<a name="207567961"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207567961" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207567961">(Aug 20 2020 at 20:02)</a>:</h4>
<p>linking to cppreference or llvm docs would be a reasonable stopgap</p>



<a name="207569248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207569248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207569248">(Aug 20 2020 at 20:14)</a>:</h4>
<p>Yeah, LLVM does better explain the memory orderings than C11 docs, because it literally says what optimizer can and can't do</p>



<a name="207569875"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207569875" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207569875">(Aug 20 2020 at 20:21)</a>:</h4>
<p>I'm hoping that the unsafe code guidelines group eventually gets around to defining this memory model better than C++ did. I thought my C++ language lawyering days were over</p>



<a name="207570025"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207570025" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207570025">(Aug 20 2020 at 20:22)</a>:</h4>
<p>C11 memory ordering docs say, that this code</p>
<div class="codehilite"><pre><span></span><code><span class="c1">// Thread 1</span>
<span class="n">x</span><span class="p">.</span><span class="n">store</span><span class="p">(</span><span class="mi">42</span><span class="p">,</span><span class="w"> </span><span class="n">Ordering</span>::<span class="n">Release</span><span class="p">);</span><span class="w"></span>
<span class="n">x</span><span class="p">.</span><span class="n">store</span><span class="p">(</span><span class="mi">43</span><span class="p">,</span><span class="w"> </span><span class="n">Ordering</span>::<span class="n">Relaxed</span><span class="p">);</span><span class="w"></span>
<span class="c1">// Thread 2, later</span>
<span class="n">println</span><span class="o">!</span><span class="p">(</span><span class="s">&quot;{}&quot;</span><span class="p">,</span><span class="w"> </span><span class="n">x</span><span class="p">.</span><span class="n">load</span><span class="p">(</span><span class="n">Ordering</span>::<span class="n">Acquire</span><span class="p">));</span><span class="w"></span>
</code></pre></div>


<p>most probably should print <code>42</code>, meanwhile I had been sure that it would be <code>43</code>, because I thought <code>Acquire</code> would look for newest write</p>
<p>Another example:</p>
<div class="codehilite"><pre><span></span><code><span class="c1">// Thread 1</span>
<span class="n">x</span><span class="p">.</span><span class="n">store</span><span class="p">(</span><span class="mi">42</span><span class="p">,</span><span class="w"> </span><span class="n">Ordering</span>::<span class="n">Release</span><span class="p">);</span><span class="w"></span>
<span class="n">x</span><span class="p">.</span><span class="n">store</span><span class="p">(</span><span class="mi">43</span><span class="p">,</span><span class="w"> </span><span class="n">Ordering</span>::<span class="n">Relaxed</span><span class="p">);</span><span class="w"></span>
<span class="c1">// Thread 2, later</span>
<span class="n">println</span><span class="o">!</span><span class="p">(</span><span class="s">&quot;{}&quot;</span><span class="p">,</span><span class="w"> </span><span class="n">x</span><span class="p">.</span><span class="n">load</span><span class="p">(</span><span class="n">Ordering</span>::<span class="n">Relaxed</span><span class="p">));</span><span class="w"></span>
</code></pre></div>


<p>According to docs, this should be randomly 42 or 43, but I thought that <code>Release</code> would force threads to update this value (so more probably 42 should be printed)</p>



<a name="207570692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207570692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207570692">(Aug 20 2020 at 20:29)</a>:</h4>
<p>I think both of them could print 42 or 43</p>



<a name="207570762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207570762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207570762">(Aug 20 2020 at 20:30)</a>:</h4>
<p>even if everything was <code>SeqCst</code> you would still have 42 or 43</p>



<a name="207570895"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207570895" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207570895">(Aug 20 2020 at 20:31)</a>:</h4>
<p>I don't think you can meaningfully reason about probabilities here, it really is just a set of options that the compiler / hardware is allowed to pick from</p>



<a name="207571183"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207571183" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207571183">(Aug 20 2020 at 20:33)</a>:</h4>
<p><del>Well, that would be kinda unsound, imagine locking a spinlock and then second thread comes and sees it as unlocked</del><br>
Nevermind, in spinlocks no one should use relaxed ordering anyway</p>



<a name="207571314"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207571314" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207571314">(Aug 20 2020 at 20:34)</a>:</h4>
<p>the second thread could be seeing it unlocked because the first thread hasn't run yet</p>



<a name="207571396"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207571396" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207571396">(Aug 20 2020 at 20:36)</a>:</h4>
<p>The ordering guaranteed by <code>SeqCst</code> doesn't have to match wall clock time</p>



<a name="207592635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207592635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Philipp Korber <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207592635">(Aug 21 2020 at 01:17)</a>:</h4>
<p><code>Aquire</code>/<code>Release</code> only really are useful in combination with each other if you only have an <code>Aquire</code> but no <code>Release</code> or the other way around you can treat them <em>roughly</em> as relaxed as long as no <code>SeqCst</code> is involved. Always use them as a pair. </p>
<p>Also as long as you don't know really well what you do your should always try to avoid <code>Relaxed</code> memory ordering, tbh. I would prefer an example in the rust did which doesn't use <code>Relaxed</code> ordering. But then (simple) fences usage are mainly optimizations where you do a less strict load/cas/etc. then you normally could but then "fix" that with an fence. If I remember correctly a good real world example is the usage of fences in <code>Arc</code>.</p>



<a name="207592720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207592720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Philipp Korber <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207592720">(Aug 21 2020 at 01:19)</a>:</h4>
<p>I remember a talk who one of the people which designed the C++ atomic rules mentions that they originally didn't want to add relaxed ordering at all but then had to do so for some optimizations for ARM and I think PowerPc. Sadly I haven't bookmarked it.</p>



<a name="207594422"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207594422" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207594422">(Aug 21 2020 at 02:02)</a>:</h4>
<p>Isn't <code>Relaxed</code> the correct ordering when you just want to avoid UB on data races?</p>



<a name="207594443"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207594443" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207594443">(Aug 21 2020 at 02:03)</a>:</h4>
<p>I recall the reference count on an <code>Arc</code> being a classic example of <code>Relaxed</code>, since it's not actually synchronizing with anything else</p>



<a name="207610817"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207610817" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207610817">(Aug 21 2020 at 08:34)</a>:</h4>
<p>The reference count on an <code>Arc</code> can't be used with <code>Relaxed</code> when dropping: <a href="https://github.com/rust-lang/rust/blob/b51651ae9d0161967617be930415705b2e4d5faf/library/alloc/src/sync.rs#L1329">https://github.com/rust-lang/rust/blob/b51651ae9d0161967617be930415705b2e4d5faf/library/alloc/src/sync.rs#L1329</a> <code>clone</code> can use <code>Relaxed</code> though: <a href="https://github.com/rust-lang/rust/blob/b51651ae9d0161967617be930415705b2e4d5faf/library/alloc/src/sync.rs#L1055">https://github.com/rust-lang/rust/blob/b51651ae9d0161967617be930415705b2e4d5faf/library/alloc/src/sync.rs#L1055</a></p>



<a name="207614873"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207614873" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207614873">(Aug 21 2020 at 09:32)</a>:</h4>
<p><a href="https://godbolt.org/z/M5j47M">https://godbolt.org/z/M5j47M</a><br>
Why load/store with <code>SeqCst</code> have fences on both sides?</p>



<a name="207621405"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207621405" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207621405">(Aug 21 2020 at 10:54)</a>:</h4>
<p>Arm and RISC-V have much weaker memory models then x86, meaning that those fences are necessary to guarantee sequential consistency. If there was only a fence at once side, a memory operation could be re-ordered between the fence and the memory operation the fence is next to.</p>



<a name="207623244"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207623244" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207623244">(Aug 21 2020 at 11:21)</a>:</h4>
<div class="codehilite"><pre><span></span><code><span class="n">x</span><span class="p">.</span><span class="n">store</span><span class="p">(</span><span class="mi">42</span><span class="p">,</span><span class="w"> </span><span class="n">Release</span><span class="p">);</span><span class="w"></span>
<span class="n">compiler_fence</span><span class="p">(</span><span class="n">SeqCst</span><span class="p">);</span><span class="w"></span>
<span class="kd">let</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">y</span><span class="p">.</span><span class="n">load</span><span class="p">(</span><span class="n">Acquire</span><span class="p">);</span><span class="w"></span>
</code></pre></div>


<p>This could be reordered by hardware to</p>
<div class="codehilite"><pre><span></span><code><span class="kd">let</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">y</span><span class="p">.</span><span class="n">load</span><span class="p">(</span><span class="n">Acquire</span><span class="p">);</span><span class="w"></span>
<span class="n">x</span><span class="p">.</span><span class="n">store</span><span class="p">(</span><span class="mi">42</span><span class="p">,</span><span class="w"> </span><span class="n">Release</span><span class="p">);</span><span class="w"></span>
</code></pre></div>


<p>?</p>



<a name="207623464"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207623464" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207623464">(Aug 21 2020 at 11:25)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207594443">said</a>:</p>
<blockquote>
<p>I recall the reference count on an <code>Arc</code> being a classic example of <code>Relaxed</code>, since it's not actually synchronizing with anything else</p>
</blockquote>
<p>Yeah, this is kinda tricky to understand, but there is no situation where <code>Relaxed</code> would be incorrect to use inside <code>clone</code> :D</p>



<a name="207627068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207627068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207627068">(Aug 21 2020 at 12:17)</a>:</h4>
<p><a href="https://github.com/Soveu/stacc/blob/master/src/stacc_lockfree_hp.rs">https://github.com/Soveu/stacc/blob/master/src/stacc_lockfree_hp.rs</a><br>
This is my first lock-free stack, feel free to criticize :)</p>



<a name="207633633"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207633633" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Eh2406 <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207633633">(Aug 21 2020 at 13:27)</a>:</h4>
<blockquote>
<p>Sadly I haven't bookmarked it.</p>
</blockquote>
<p>I think it is mentioned in Herb Sutter's "atomic Weapons" <a href="https://www.youtube.com/watch?v=A8eCGOqgvH4">https://www.youtube.com/watch?v=A8eCGOqgvH4</a> and <a href="https://www.youtube.com/watch?v=KeLBd2EJLOU">https://www.youtube.com/watch?v=KeLBd2EJLOU</a></p>
<div class="youtube-video message_inline_image"><a data-id="KeLBd2EJLOU" href="https://www.youtube.com/watch?v=KeLBd2EJLOU"><img src="https://i.ytimg.com/vi/KeLBd2EJLOU/default.jpg"></a></div><div class="youtube-video message_inline_image"><a data-id="A8eCGOqgvH4" href="https://www.youtube.com/watch?v=A8eCGOqgvH4"><img src="https://i.ytimg.com/vi/A8eCGOqgvH4/default.jpg"></a></div>



<a name="207727925"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207727925" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207727925">(Aug 22 2020 at 14:57)</a>:</h4>
<p><span class="user-mention silent" data-user-id="328907">Soveu</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207569248">said</a>:</p>
<blockquote>
<p>Yeah, LLVM does better explain the memory orderings than C11 docs, because it literally says what optimizer can and can't do</p>
</blockquote>
<p>While such examples are helpful to understand memory orderings, keep in mind that their actual underlying specification is <em>not</em> in terms of what the compiler can and cannot do. There is a spec of what the <em>program</em> can and cannot do when  being executed (the possible behaviors of the program), and the compiler can only do things that do not change program behavior. Thus, a really smart compiler can do way more than what these simple examples might suggest. for example, if the compiler can prove that an atomic location is only used from a single thread, it may replace all atomic accesses by non-atomic accesses.</p>



<a name="207728055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207728055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207728055">(Aug 22 2020 at 15:00)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207570895">said</a>:</p>
<blockquote>
<p>I don't think you can meaningfully reason about probabilities here, it really is just a set of options that the compiler / hardware is allowed to pick from</p>
</blockquote>
<p>indeed. this is <em>non-determinism</em>, which is very distinct from randomness. it just means that every execution will make one of the allowed choices, but says nothing about which choice is observed how often when you execute the program many times. this distribution is entirely unspecified and can be affected by random hardware effects (e.g. alignment of the memory involved), compiler optimizations, indirect interactions with other code running in parallel, ...</p>



<a name="207736335"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207736335" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207736335">(Aug 22 2020 at 18:29)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> By the way, I've been thinking of writing a precise memory model, probably in blog like form at first (although I don't have a blog), that can eventually serve as our replacement for "we do what C++11 does" because that's a terrible way to specify anything, and after reading <a href="https://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf">several</a> <a href="https://people.mpi-sws.org/~viktor/papers/oopsla2013-rsl.pdf">papers</a> on mathematizing the C++11 concurrency spec, it turns out they messed up pretty badly when it comes to relaxed atomics, allowing causal loops that make it impossible to prove anything about program behavior while still not being UB.</p>
<p>I have a background in formal proof assistants and formal verification, but I haven't actually participated in WG-UCG before. Where would be a good place to build such information?</p>



<a name="207774675"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207774675" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207774675">(Aug 23 2020 at 13:59)</a>:</h4>
<p>yeah, the C11 model has many problems, but so far no clearly superior model has surfaced despite many years of research. there are some exciting proposals though, I really like the "promising semantics" (<a href="https://people.mpi-sws.org/~viktor/papers/popl2017-promising.pdf">original paper</a>, <a href="http://www.cse.iitd.ac.in/~soham/publications/promising2.pdf">this years follow-up</a>).</p>



<a name="207774821"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207774821" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207774821">(Aug 23 2020 at 14:02)</a>:</h4>
<p>regarding your last question, not sure -- blog posts are a great start.</p>



<a name="207774834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207774834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207774834">(Aug 23 2020 at 14:02)</a>:</h4>
<p>eventually putting it into paper format for peer review might also be a good idea, but that's probably still ways off ;)</p>



<a name="207776721"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207776721" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207776721">(Aug 23 2020 at 14:48)</a>:</h4>
<p>If I could only understand this language <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span> <a href="/user_uploads/4715/CpQTqpE4mXx78y5Hm-3SM_pX/Screenshot-from-2020-08-23-16-47-27.png">Screenshot-from-2020-08-23-16-47-27.png</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/CpQTqpE4mXx78y5Hm-3SM_pX/Screenshot-from-2020-08-23-16-47-27.png" title="Screenshot-from-2020-08-23-16-47-27.png"><img src="/user_uploads/4715/CpQTqpE4mXx78y5Hm-3SM_pX/Screenshot-from-2020-08-23-16-47-27.png"></a></div>



<a name="207780722"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207780722" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Poliorcetics <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207780722">(Aug 23 2020 at 16:33)</a>:</h4>
<p>I find it beautiful while still not understanding a word of what is written in the screenshot</p>



<a name="207784042"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207784042" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207784042">(Aug 23 2020 at 17:55)</a>:</h4>
<p>Yeah, this looks similar to notation in other compiler/language related papers (like in the Ralf's paper about LLVM <code>no_alias</code>)</p>



<a name="207785961"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207785961" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207785961">(Aug 23 2020 at 18:45)</a>:</h4>
<p>I think a good next step in this area is a description of a semantics with good formal properties, which is understandable to mere mortals. The "pages of fractions" are important for formal folks but a sound underapproximation under certain assumptions (e.g. SC-DRF, use message passing like this and don't touch atomics and you will be fine, etc.). Even a fully precise model should be describable in prose in a few pages at most (the C++ committee always manages to screw this part up)</p>



<a name="207786008"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207786008" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207786008">(Aug 23 2020 at 18:47)</a>:</h4>
<p>After some reading I think there has been enough legwork done on better C11 semantics already, I doubt I can do a better job</p>



<a name="207786015"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207786015" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207786015">(Aug 23 2020 at 18:47)</a>:</h4>
<p>but explaining what already exists in one place would still be very useful</p>



<a name="207788397"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207788397" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Soveu <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207788397">(Aug 23 2020 at 19:49)</a>:</h4>
<p>RISC-V has nice and simple atomics</p>



<a name="207790022"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207790022" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207790022">(Aug 23 2020 at 20:32)</a>:</h4>
<p>(oops, when I said don't touch atomics I meant relaxed atomics. Guess you can't edit posts here?)</p>



<a name="207790431"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207790431" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207790431">(Aug 23 2020 at 20:43)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207785961">said</a>:</p>
<blockquote>
<p>I think a good next step in this area is a description of a semantics with good formal properties, which is understandable to mere mortals. The "pages of fractions" are important for formal folks but a sound underapproximation under certain assumptions (e.g. SC-DRF, use message passing like this and don't touch atomics and you will be fine, etc.). Even a fully precise model should be describable in prose in a few pages at most (the C++ committee always manages to screw this part up)</p>
</blockquote>
<p>Part of the problem is that sequential consistency is not enough to write the highest-performance concurrent data structures. It's harder (but still quite possible) to specify semantics allowing for concurrency that doesn't force SC.</p>



<a name="207790573"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207790573" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207790573">(Aug 23 2020 at 20:46)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207790022">said</a>:</p>
<blockquote>
<p>(oops, when I said don't touch atomics I meant relaxed atomics. Guess you can't edit posts here?)</p>
</blockquote>
<p>only for an hour I think</p>



<a name="207791591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207791591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207791591">(Aug 23 2020 at 21:11)</a>:</h4>
<p>Right, I'm really thinking of semantics for "the land below SC". SC itself is fairly well understood</p>



<a name="207791757"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207791757" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207791757">(Aug 23 2020 at 21:15)</a>:</h4>
<p>My impression of the field matches up with what Ralf said. C11 semantics is <a href="https://fzn.fr/readings/c11comp.pdf">known to be broken</a>, and there are several proposals for alternatives which fix many of the issues, but every proposal invalidates some compiler or hardware technique (which shouldn't be too surprising because the whole business is currently inconsistent), so we have to figure out which things we are willing to part with</p>



<a name="207794245"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794245" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794245">(Aug 23 2020 at 22:29)</a>:</h4>
<p><span class="user-mention" data-user-id="271719">@Mario Carneiro</span> The fundamental premise of the C11 semantics were "what people are doing is OK, so how do we specify it". Any potential replacement would need to start with the same premise, or people who need to continue doing what they're doing cannot use that replacement.</p>



<a name="207794323"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794323" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794323">(Aug 23 2020 at 22:31)</a>:</h4>
<p>A better model may allow more compiler techniques without breaking programs, but the premise should always be "how can we allow more optimization without invalidating programs that work on real hardware", not "which additional valid programs are we willing to start rejecting".</p>



<a name="207794363"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794363" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794363">(Aug 23 2020 at 22:32)</a>:</h4>
<p>Of course. The problem is that because there was not a rigid specification of what the contract was, different optimizations make different assumptions and the result is an unambiguously buggy combination of individually okay-looking things. Any attempt to put a coherent global structure on this is going to have to reject one of those things</p>



<a name="207794376"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794376" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794376">(Aug 23 2020 at 22:33)</a>:</h4>
<p>I think I'm missing something. Going by the title and abstract of the paper you linked, it sounds like C11 has specified semantics, those semantics just disallow certain compiler optimizations.</p>



<a name="207794380"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794380" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794380">(Aug 23 2020 at 22:33)</a>:</h4>
<p>Or am I misunderstanding the paper?</p>



<a name="207794382"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794382" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794382">(Aug 23 2020 at 22:33)</a>:</h4>
<p>They disallow optimizations that were explicitly intended to be okay by the designers of the C11 standard</p>



<a name="207794423"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794423" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794423">(Aug 23 2020 at 22:34)</a>:</h4>
<p>in other words, they failed to meet their own criteria</p>



<a name="207794429"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794429" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794429">(Aug 23 2020 at 22:34)</a>:</h4>
<p>Ah, <em>that</em> is the information I was missing, thank you.</p>



<a name="207794432"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794432" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794432">(Aug 23 2020 at 22:34)</a>:</h4>
<p>which is why I am comfortable saying that the standard is broken without further qualification</p>



<a name="207794439"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794439" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794439">(Aug 23 2020 at 22:35)</a>:</h4>
<p>In the abstract, it would have helped to change "and that are deemed to be correct" to "and that were intended to be allowed by the C11 model".</p>



<a name="207794452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794452">(Aug 23 2020 at 22:35)</a>:</h4>
<p>For example, in the Herb Sutter talk linked above, there is explicit reference to so called "roach motel reorderings" that were proven invalid in that paper</p>



<a name="207794506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794506">(Aug 23 2020 at 22:37)</a>:</h4>
<p>Also I haven't found a direct reference but the papers seem to suggest that SC-DRF is known to not hold in C11</p>



<a name="207794515"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794515" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794515">(Aug 23 2020 at 22:37)</a>:</h4>
<p><em>That</em> much is entirely intended, as far as I know. The C11 semantics are not supposed to be limited to sequential consistency.</p>



<a name="207794525"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794525" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794525">(Aug 23 2020 at 22:37)</a>:</h4>
<p>When using relaxed atomics, I mean.</p>



<a name="207794526"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794526" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794526">(Aug 23 2020 at 22:37)</a>:</h4>
<p>No, I mean if you use SC atomics</p>



<a name="207794565"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794565" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794565">(Aug 23 2020 at 22:38)</a>:</h4>
<p>Of course if you use relaxed atomics you get what you deserve, but SC atomics aren't properly SC</p>



<a name="207794572"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794572" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794572">(Aug 23 2020 at 22:38)</a>:</h4>
<p>this is the sort of basic coherence failure that indicates that the model has gone horribly wrong somewhere</p>



<a name="207794582"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794582" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794582">(Aug 23 2020 at 22:39)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207794526">said</a>:</p>
<blockquote>
<p>No, I mean if you use SC atomics</p>
</blockquote>
<p>Now <em>that's</em> weird; I'd love to see some details on that.</p>



<a name="207794586"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794586" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794586">(Aug 23 2020 at 22:39)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207794565">said</a>:</p>
<blockquote>
<p>Of course if you use relaxed atomics you get what you deserve, but SC atomics aren't properly SC</p>
</blockquote>
<p>Please don't denigrate non-SC code with comments like "you get what you deserve"; relaxed atomics exist for a reason, to support valid program implementations.</p>



<a name="207794707"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794707" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794707">(Aug 23 2020 at 22:42)</a>:</h4>
<p>I'm being tongue in cheek. Of course I would like to have good support for relaxed atomics, so I can use them and know what they mean. C11 relaxed atomics are magical time travelers</p>



<a name="207794710"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794710" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794710">(Aug 23 2020 at 22:42)</a>:</h4>
<p><a href="https://people.mpi-sws.org/~dreyer/papers/scfix/paper.pdf">https://people.mpi-sws.org/~dreyer/papers/scfix/paper.pdf</a> has a big section on problems with SC atomics</p>



<a name="207794768"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794768" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794768">(Aug 23 2020 at 22:44)</a>:</h4>
<p>For a little background here, to provide some context for why this is a sensitive topic: when the C11 model was being introduced, it was very much a tooth-and-nail uphill battle against folks who basically said anything that isn't sequential consistency is just flatly unacceptable and wrong.</p>



<a name="207794904"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794904" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794904">(Aug 23 2020 at 22:48)</a>:</h4>
<p>I don't know if release-acquire is the best primitive for message passing but it's at least somewhat comprehensible. It would also be nice if there was an "unsynchronized read/write" primitive that you can compile to plain (atomic) reads and writes. I'm still reading the promising papers but it does seem to solve a lot of problems</p>



<a name="207794966"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794966" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794966">(Aug 23 2020 at 22:50)</a>:</h4>
<p>SC is a nice model, but it unfortunately doesn't really reflect hardware at all. They basically get compiled to fences after every instruction on most architectures</p>



<a name="207794967"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794967" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794967">(Aug 23 2020 at 22:50)</a>:</h4>
<p>/me nods to that last bit.</p>



<a name="207794978"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207794978" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207794978">(Aug 23 2020 at 22:51)</a>:</h4>
<p>To the best of my knowledge, the semantics of relaxed atomics are <em>supposed</em> to be, roughly, that there won't be any load-tearing or store-tearing (you'll get the old or the new value), and that any given thread that reads the new value won't start reading the old value again, and otherwise there's no ordering guarantee unless you separately apply additional barriers.</p>



<a name="207795026"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795026" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795026">(Aug 23 2020 at 22:52)</a>:</h4>
<p>LLVM actually has an "even more relaxed" atomic operation called <code>Unordered</code>, where "relaxed" is <code>Monotonic</code>. The main difference is that relaxed writes to the same location are totally ordered by the "modification order" to that location</p>



<a name="207795128"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795128" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795128">(Aug 23 2020 at 22:55)</a>:</h4>
<p>That is, if two threads A and B relaxed write to location X, it is not possible for threads C and D to each see both writes in opposite orders</p>



<a name="207795142"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795142" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795142">(Aug 23 2020 at 22:55)</a>:</h4>
<p>but with unordered writes that's possible</p>



<a name="207795204"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795204" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795204">(Aug 23 2020 at 22:57)</a>:</h4>
<p>Fair enough. The concurrent algorithms I work with tend to care more about relaxed reads, and tend to synchronize writes; the idea of racing two relaxed writes against each other doesn't seem nearly as common.</p>



<a name="207795465"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795465" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795465">(Aug 23 2020 at 23:02)</a>:</h4>
<p>(Such programs still use relaxed writes, but do so inside critical sections.)</p>



<a name="207795558"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795558" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795558">(Aug 23 2020 at 23:05)</a>:</h4>
<p>I don't like that the C11 primitives have such complicated codegen. I would like the lowest level operations to lower to individual reads, writes and fences if possible.</p>



<a name="207795562"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795562" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795562">(Aug 23 2020 at 23:05)</a>:</h4>
<p>unfortunately that sort of thing is not very portable</p>



<a name="207795615"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207795615" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207795615">(Aug 23 2020 at 23:06)</a>:</h4>
<p>Definite agreement there.</p>



<a name="207931082"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207931082" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207931082">(Aug 25 2020 at 07:14)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207791591">said</a>:</p>
<blockquote>
<p>Right, I'm really thinking of semantics for "the land below SC". SC itself is fairly well understood</p>
</blockquote>
<p>SC on its own is. Mixing SC and "lower" atomic accesses on the same location is actually very poorly understood (and there were some bugs there that the next C++ will fix).</p>



<a name="207931094"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207931094" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207931094">(Aug 25 2020 at 07:14)</a>:</h4>
<p><span class="user-mention silent" data-user-id="328907">Soveu</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207788397">said</a>:</p>
<blockquote>
<p>RISC-V has nice and simple atomics</p>
</blockquote>
<p>unfotunately that does not help when specifying a <em>language</em> memory model. when it comes to concurrency, hardware and language models are entirely different beasts.</p>



<a name="207931128"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207931128" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207931128">(Aug 25 2020 at 07:15)</a>:</h4>
<p>hardware model tend to take into account syntactic dependencies ("if an operation has this register as an input, it counts as being data-dependent on the last thing that wrote to that register"). this is a trick that is impossible to pull in language models where compilers routinely optimize <code>x*0</code> to <code>0</code>, thus removing such data dependencies.</p>



<a name="207931142"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207931142" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207931142">(Aug 25 2020 at 07:15)</a>:</h4>
<p>this is why the C++11 "consume" ordering is entirely broken -- nobody knows how to say anything precise about it</p>



<a name="207931230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207931230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207931230">(Aug 25 2020 at 07:17)</a>:</h4>
<p>if we didnt care for relaxed, we'd have a <em>beautiful</em> model already, the SRA model: <a href="https://plv.mpi-sws.org/sra/paper.pdf">https://plv.mpi-sws.org/sra/paper.pdf</a></p>



<a name="207931430"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207931430" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207931430">(Aug 25 2020 at 07:20)</a>:</h4>
<p>this has an axiomatic and an operational model (proven equivalent), both are reaosnably simple, there are coq proofs of all relevant reorderings. While we don't have a fully "canonical" program logic yet, but we do have several years of work across various papers that build program logics for semantics like this, including one that shows soundness of a bunch of core Rust abstractions (<a href="https://people.mpi-sws.org/~dreyer/papers/rbrlx/paper.pdf">https://people.mpi-sws.org/~dreyer/papers/rbrlx/paper.pdf</a>).<br>
as that last paper shows we even know how to extend this reasonably well with a form of relaxed accesses that is strictly weaker than release/acquire. but these relaxed accesses still do not allow one key optimization (load buffering I think), and it is adding that optimization which kills <em>everything</em>. of course this also means that the only "sensible" relaxed semantics we have (in terms of having a not-completely-crazy spec and a reasonable program logic) cannot be compiled without fences -- so some might not call it "sensible" after all.</p>



<a name="207931671"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207931671" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207931671">(Aug 25 2020 at 07:24)</a>:</h4>
<p>(I should also note that these are my opinion are not necessarily consensus in my research community. ;) there are various contenders for relaxed semantics, not just the crazy complicated "promising" semantics, but the others are very axiomatic in their style so I have a hard time really building any intuition for what they <em>mean</em>. AFAIK none of them comes with a program logic.)</p>



<a name="207932336"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207932336" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207932336">(Aug 25 2020 at 07:34)</a>:</h4>
<p>After reading the "promising" papers, I agree that it is a very nice model. The fact that it is very operational is a bit of a downside though</p>



<a name="207932398"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207932398" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207932398">(Aug 25 2020 at 07:35)</a>:</h4>
<p>Ideally you would have both styles and a proof of equivalence. I don't know whether that's a prerequisite, but it's a big plus</p>



<a name="207932553"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207932553" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207932553">(Aug 25 2020 at 07:37)</a>:</h4>
<p>Do you know whether the promising model's RA fragment matches the SRA model?</p>



<a name="207932676"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207932676" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207932676">(Aug 25 2020 at 07:39)</a>:</h4>
<p>My reading list has grown once again :)</p>



<a name="207974059"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207974059" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207974059">(Aug 25 2020 at 15:00)</a>:</h4>
<p>I consider being operational a big advantage. I never was able to wrap my head around these axiomatic models. The first time I understood RA was when reading the SRA paper. ;)</p>



<a name="207974121"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207974121" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207974121">(Aug 25 2020 at 15:00)</a>:</h4>
<p>IMO the axiomatic models are nice properties to show about an operational model, but I feel that the "ground truth" of <em>program execution</em> should be operational. It's supposed to reflect a computation after all.</p>



<a name="207974165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207974165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207974165">(Aug 25 2020 at 15:01)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/122651-general/topic/Understanding.20atomic.20ordering/near/207932553">said</a>:</p>
<blockquote>
<p>Do you know whether the promising model's RA fragment matches the SRA model?</p>
</blockquote>
<p>No, AFAIK it matches a slight tweak of the SRA model to make it equivalent to C++11 RA. It's easy to adjust SRA accordingly, which is useful when selling this to people that are already sold on C++11 RA (so, good for getting things published) -- but I think SRA is the nicer model, as they convincingly demonstrated.^^<br>
So, SRA vs "weak" (normal) RA is a decision that's orthogonal to handling relaxed accesses. If I recall correctly, both the operational and axiomatic model are easy to tweak one way or the other.</p>



<a name="207981965"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/207981965" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#207981965">(Aug 25 2020 at 16:00)</a>:</h4>
<p>I think an operational model loses some advantage when it (like the promising model) is performing arbitrary amounts of counterfactual computation on every step and also filling in bits of the "past" and "future" as it goes. (Given the way Stacked Borrows is defined, I already inferred that you have a great preference for operational models.) A declarative model is useful for being able to tell what properties hold globally, but operational models help with setting up an order to prove properties, and providing a reliable direction of "time" that can be reasoned about. But like I said it is best when you have both views, so you can exploit the advantages of each.</p>
<p>On that note, is there a nondeterministic model of stacked borrows? It would be easier to see the stack as lifetimes again if the machine could nondeterministically end a borrow at appropriate points, and having all these stacks on memory locations might be good for an interpreter like miri but is like looking at a program in CPS, everything seems to be inside out from the regular way things are viewed. (For example, lifetimes quantify over future times when a value will be destroyed, but your <code>Shr</code> nodes instead store a point in the past when the lifetime was first established.)</p>



<a name="208059278"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208059278" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208059278">(Aug 26 2020 at 07:14)</a>:</h4>
<p>If the operational model has to do crazy things like hypothetical executions (is that what you mean by "counterfactual"?), then that just shows that the semantics are crazy. The axiomatic model has all the same craziness, it's just hidden better. Hiding craziness is not an advantage, it's a flaw of the axiomatic model that prevents actually understanding what happens, at least for me.</p>



<a name="208059311"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208059311" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208059311">(Aug 26 2020 at 07:15)</a>:</h4>
<p>I agree it is best to have both views, so I can ignore the axiomatic model as I do not understand it, but I can still talk to people that prefer that view. ;)</p>



<a name="208059373"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208059373" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208059373">(Aug 26 2020 at 07:16)</a>:</h4>
<p>Also as a matter of principle, when it comes to <em>defining</em> the very meaning of "executing a Rust program", I would not accept anything axiomatic. Executing a program is an operational affair.</p>



<a name="208059408"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208059408" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208059408">(Aug 26 2020 at 07:17)</a>:</h4>
<blockquote>
<p>On that note, is there a nondeterministic model of stacked borrows? It would be easier to see the stack as lifetimes again if the machine could nondeterministically end a borrow at appropriate points, and having all these stacks on memory locations might be good for an interpreter like miri but is like looking at a program in CPS, everything seems to be inside out from the regular way things are viewed. (For example, lifetimes quantify over future times when a value will be destroyed, but your Shr nodes instead store a point in the past when the lifetime was first established.)</p>
</blockquote>
<p>I don't know of such a model, and I doubt I'd be able to build it as that's just not how my intuition works.<br>
Also I do not see the relationship to CPS at all, Stacked Borrows doesn't invert control (or anything else) in any way that I can see? My stack items track which lifetimes are still active, and I keep all lifetimes active as long as possible. IMO that's exactly the regular way to view lifetimes -- figuring out which of them are still alive.</p>



<a name="208060288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208060288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208060288">(Aug 26 2020 at 07:29)</a>:</h4>
<blockquote>
<p>I don't know of such a model, and I doubt I'd be able to build it as that's just not how my intuition works.</p>
</blockquote>
<p>Okay, then I think I have an upcoming blog post for you :)</p>



<a name="208272160"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208272160" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208272160">(Aug 27 2020 at 20:32)</a>:</h4>
<p><span class="user-mention" data-user-id="271719">@Mario Carneiro</span> I talked with a friend on the C and C++ standards committee today.</p>



<a name="208272188"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208272188" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208272188">(Aug 27 2020 at 20:32)</a>:</h4>
<p>He was familiar with both of the papers you'd linked to.</p>



<a name="208272297"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208272297" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208272297">(Aug 27 2020 at 20:33)</a>:</h4>
<p>The paper "Repairing  Sequential  Consistency  in  C/C++11" accurately describes a bug in the C11 memory model, specifically in regards to POWER, which will be fixed in C20.</p>



<a name="208272383"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208272383" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208272383">(Aug 27 2020 at 20:34)</a>:</h4>
<p>For the other paper, those issues are a subject of ongoing discussion in the C standards committee.</p>



<a name="208272420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208272420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208272420">(Aug 27 2020 at 20:34)</a>:</h4>
<p>There's some work happening in that area, but it sounds less likely that it'll be addressed soon.</p>



<a name="208272541"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208272541" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208272541">(Aug 27 2020 at 20:35)</a>:</h4>
<p>It also sounds like part of the problem is that the C11 memory model was lax enough to allow some excessively aggressive optimizations by compiler authors, and some of those folks are fighting to keep that despite it breaking real-world programs.</p>



<a name="208272666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208272666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208272666">(Aug 27 2020 at 20:36)</a>:</h4>
<p>(On the flip side, there are some programs that legitimately want such optimizations, and either don't care about parallelism or don't care about security, and for some reason don't want to have to pass a compiler option enabling that.)</p>



<a name="208278525"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Understanding%20atomic%20ordering/near/208278525" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Understanding.20atomic.20ordering.html#208278525">(Aug 27 2020 at 21:24)</a>:</h4>
<p>Yeah, I think some of this warrants a <code>--ftimey-wimey</code> compiler flag to turn on dubious optimizations that people can't bear to part with but have no reasonable semantic meaning, analogous to <code>--ffast-math</code></p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>